(declare-fun v2 () Bool)
(declare-fun r0 () Real)
(declare-fun str5 () String)
(declare-fun str9 () String)
(assert (str.in_re str5 re.allchar))
(assert (or v2 (str.< str5 str9)))
(assert (or (= 0 r0) (not (= str9 (str.replace_re_all str9 re.all (str.from_int (str.len str9)))))))
(push)
(check-sat)
(pop)
(assert (< 0 r0))
(check-sat)
